|
|
Obsluha paměťového systému pro platformu Colibri XScale PXA270
Mačišák, Lukáš ; Straka, Martin (oponent) ; Šimek, Václav (vedoucí práce)
Tato bakalářská práce popisuje platformu Colibri XScale PXA270, analyzuje možnosti využití DMA přenosů na této platformě a popisuje principy práce s paměťmi typu flash a SDRAM. Práce obsahuje návrh a implementaci firmware pro obsluhu paměťového systému této platformy. Součástí práce je i popis a implementace testů polovodičových pamětí s přímým přístupem. Pro ukázku funkčnosti a možností použití firmware je implementována demonstrační aplikace.
|
|
|
Návrh testeru paměti RAM ve VHDL
Charvát, Jiří ; Straka, Martin (oponent) ; Strnadel, Josef (vedoucí práce)
Tato práce popisuje problematiku hardwarového testování polovodičových pamětí. Popisuje princip fungování základních typů pamětí, způsob, jakým uchovávají data a způsob komunikace. Dále ukazuje typické poruchy, které v těchto pamětech mohou nastat. Součástí je také návrh a implementace modelu paměti a testeru v jazyce VHDL. Do paměti je možné zanést chyby a následně je připojeným testerem odhalit. Závěrem je nastíněno, jaká je úspěšnost při detekci různých druhů chyb použitím různých druhů testů. Zaměřuje se hlavně na detekci chyb pomocí march testu a jeho variant.
|
|
|
Program Loop Unwinding in the 2LS Framework
Nečas, František ; Vojnar, Tomáš (oponent) ; Malík, Viktor (vedoucí práce)
The goal of this work is to propose an improved unwinding mechanism for the 2LS formal verification tool. 2LS is a static analysis framework for C programs based on reasoning about programs using an SMT solver. It combines multiple common verification techniques into an algorithm called k I k I. One of the crucial parts of the algorithm is loop unwinding. Unfortunately, the existing solution does not correctly support unwinding of loops containing operations with dynamically allocated memory. Our proposed solution is based on unwinding loops in a GOTO program rather than the SSA form, making it possible to correctly handle dynamic objects and operations over them. The proposed solution has been implemented in the 2LS framework and our experiments on a set of benchmarks from the International Competition on Software Verification (SV-COMP) show that it improves soundness of analysis of programs working with dynamic objects.
|
|
|
Program Loop Unwinding in the 2LS Framework
Nečas, František ; Vojnar, Tomáš (oponent) ; Malík, Viktor (vedoucí práce)
The goal of this work is to propose an improved unwinding mechanism for the 2LS formal verification tool. 2LS is a static analysis framework for C programs based on reasoning about programs using an SMT solver. It combines multiple common verification techniques into an algorithm called k I k I. One of the crucial parts of the algorithm is loop unwinding. Unfortunately, the existing solution does not correctly support unwinding of loops containing operations with dynamically allocated memory. Our proposed solution is based on unwinding loops in a GOTO program rather than the SSA form, making it possible to correctly handle dynamic objects and operations over them. The proposed solution has been implemented in the 2LS framework and our experiments on a set of benchmarks from the International Competition on Software Verification (SV-COMP) show that it improves soundness of analysis of programs working with dynamic objects.
|
|
|
Obsluha paměťového systému pro platformu Colibri XScale PXA270
Mačišák, Lukáš ; Straka, Martin (oponent) ; Šimek, Václav (vedoucí práce)
Tato bakalářská práce popisuje platformu Colibri XScale PXA270, analyzuje možnosti využití DMA přenosů na této platformě a popisuje principy práce s paměťmi typu flash a SDRAM. Práce obsahuje návrh a implementaci firmware pro obsluhu paměťového systému této platformy. Součástí práce je i popis a implementace testů polovodičových pamětí s přímým přístupem. Pro ukázku funkčnosti a možností použití firmware je implementována demonstrační aplikace.
|
|
|
Návrh testeru paměti RAM ve VHDL
Charvát, Jiří ; Straka, Martin (oponent) ; Strnadel, Josef (vedoucí práce)
Tato práce popisuje problematiku hardwarového testování polovodičových pamětí. Popisuje princip fungování základních typů pamětí, způsob, jakým uchovávají data a způsob komunikace. Dále ukazuje typické poruchy, které v těchto pamětech mohou nastat. Součástí je také návrh a implementace modelu paměti a testeru v jazyce VHDL. Do paměti je možné zanést chyby a následně je připojeným testerem odhalit. Závěrem je nastíněno, jaká je úspěšnost při detekci různých druhů chyb použitím různých druhů testů. Zaměřuje se hlavně na detekci chyb pomocí march testu a jeho variant.
|
host ::
RSS.